effect-p(es; i; ds; k; T; x; f)
== ((x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
==  subtype_rel(es-kindtype(es; i; k); T)
==  es-dtype(es; i; x; fpf-cap(ds; id-deq; x; top)))
== c alle-at(es;
== c alle-at(i;
== c alle-at(e.((es-kind(es; e) = k)
== c alle-at( (subtype_rel(es-valtype(es; e); T)
== c alle-at( c (es-after(es; x; e) = f(es-state-when(es; e),es-val(es; e)))))) 

latex

---

clarification:

effect-p(es; i; ds; k; T; x; f)
== ((x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
==  subtype_rel(es-kindtype(es; i; k); T)
==  es-dtype(es; i; x; fpf-cap(ds; id-deq; x; top)))
== c alle-at(es;
== c alle-at(i;
== c alle-at(e.((es-kind(es; e) = k  Knd)
== c alle-at( (subtype_rel(es-valtype(es; e); T)
== c alle-at( c (es-after(es; x; e)
== c alle-at( c (=
== c alle-at( c (f(es-state-when(es; e),es-val(es; e))
== c alle-at( c ( fpf-cap(ds; id-deq; x; top))))) 

latex

Definitions	x:A. B(x), Id, es-vartype(es; i; x), P  Q, es-kindtype(es; i; k), es-dtype(es; i; x; T), alle-at(es; i; e.P(e)), P  Q, Knd, es-kind(es; e), A c B, es-valtype(es; e), s = t, fpf-cap(f; eq; x; z), id-deq, top, es-after(es; x; e), f(a), es-state-when(es; e), es-val(es; e)
FDL editor aliases	effect-p